-
Notifications
You must be signed in to change notification settings - Fork 260
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Compute matching patterns for automatic induction #5835
Open
RustanLeino
wants to merge
17
commits into
dafny-lang:master
Choose a base branch
from
RustanLeino:triggers-for-auto-induction
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
feat: Compute matching patterns for automatic induction #5835
RustanLeino
wants to merge
17
commits into
dafny-lang:master
from
RustanLeino:triggers-for-auto-induction
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Conflicts: # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
# Conflicts: # Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs # Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR aims to help stabilize verification by filling in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. It also suppresses the generation of the induction hypothesis if no such matching patterns are found.
Full description
This PR computes matching patterns for the quantification that's about to be used with automatic induction. If there are no matching patterns, the induction hypothesis is not added. Tooltips or warnings show the patterns or announce the lack thereof.
The PR no longer uses arrow-typed variables as induction variables. (If a user really wants them, an
{:induction ...}
attribute can be given manually.)Treat
this
more like other parameters when computing induction variables.With this PR, ternary expressions (that is,
_ ==#[_] _
and_ !=#[_] _
) are considered as candidate trigger expressions. In addition, a codatatype==
(which is defined by Dafny as a greatest predicate) is considered as a focal predicate for extreme predicates.The PR also fixes a crash in trigger selection when the candidate expression has a lambda expression.
Finally, the "selected trigger" tooltip is extended to also show the
t := e
binding for any bound variable added as part of a quantifier rewrite.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.